Definitions | t T, Valtype(da;k), KindDeq, Knd, x:A. B(x), (x l), b, Prop, A,  b, , deq-member(eq;x;L), P  Q, P & Q, P  Q, Unit, event-info(ds;da), State(ds), Top, f(x)?z, if b t else f fi,  x,y. t(x;y), list_accum(x,a.f(x;a);y;l), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-trans-state-from(v;z;L), ecl-trans-type(A), ecl-trans-tuple{i:l}(ds;da), Id,  x. t(x), a:A fp B(a) |